Nuprl Lemma : compat-cons
0,22
postcript
pdf
T
:Type,
as
,
bs
:
T
List,
a
,
b
:
T
.
a
.
as
||
b
.
bs
a
=
b
&
as
||
bs
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
l1
||
l2
,
Prop
,
P
&
Q
,
P
Q
,
P
Q
,
P
Q
,
P
Q
,
l1
l2
,
{
T
}
Lemmas
iseg
wf
,
cons
iseg
,
compat
wf
origin
T:Type, as, bs:T List, a, b:T. a.as || b.bs 
a = b & as || bs T:Type, as, bs:T List, a, b:T. a.as || b.bs a = b & as || bs 
Tx:A. B(x)
Q Q Q
Q
l2